x, x':(), r1, r2:, k:, y:( List).
(k  ||y||)
 q-rel(r1;q-linear(k;j.x(j);y))
 q-rel(r2;q-linear(k;j.x'(j);y))
 q-rel(q-rel-lub(r1;r2);q-linear(k;j.(x(j)) + (x'(j));y)) 

latex

Definitions

p  q, if b then t else f fi , ff, tt, (i = j), q-rel-lub(r1;r2), q-rel(r;x), P & Q, True, T, x. t(x), , t  T, P  Q, P  Q, P  Q, x:A. B(x), Unit, , False, {T}, A, x(s), , , S  T

Lemmas

qle weakening eq qorder, mon ident q, qadd comm q, not functionality wrt iff, assert of bnot, eqff to assert, assert of eq int, eqtt to assert, iff transitivity, qless transitivity, qless transitivity 2 qorder, qless transitivity 1 qorder, qle transitivity qorder, qless wf, qadd preserves qless, qle wf, qadd preserves qle, not wf, bnot wf, int inc rationals, qadd wf, assert wf, bool wf, eq int wf, q-linear-sum, q-rel-lub wf, true wf, squash wf, q-linear wf, q-rel wf, length wf1, le wf, rationals wf, nat wf